\documentclass[a4paper,10pt]{article}
\usepackage[portuges]{babel}
\usepackage[latin1]{inputenc}
\usepackage{default}
\usepackage{graphicx}
\usepackage{array}
\usepackage{fullpage}
\usepackage{verbatim}
\usepackage{xcolor}
\usepackage{xypic}
\usepackage{pstricks}
\usepackage{amssymb} 


\newcommand{\rotimes}{\textcolor{red}{\blacklozenge}}
\newcommand{\gotimes}{\textcolor{green}{\blacklozenge}}

\parindent=0pt
\parskip=2pt

%opening
\title{Modela\c{c}\~ao de Esta\c{c}\~oes de Comboios - Parte II}
\author{Jo\~ao Paz \and Pedro Ara\'ujo}

\begin{document}

\maketitle

\tableofcontents

\newpage

\section{S\'intese do Problema}

Ap\'os a modela\c{c}\~ao de esta\c{c}\~oes de comboios em Alloy a seguinte etapa foi passar esse modelo para um programa em Java, usando a ferramenta ESC/Java2 (``Extended Static Checker for Java'') para testar as invariantes, pr\'e e p\'os condi\c{c}\~oes entre outras especifica\c{c}\~oes do programa enquanto escrevemos o c\'odigo. De seguida compilar o JML (``Java Modeling Language'') para encontrar poss\'iveis falhas na implementa\c{c}\~ao em tempo de execu\c{c}\~ao. 

Neste relat\'orio:
\begin{itemize}
 \item Vamos mostrar como passamos das assinaturas em Alloy para classes em Java, como implementamos as regras, invariantes e opera\c{c}\~oes em Java e a diferen\c{c}a entre o c\'odigo Alloy e Java;
 \item Vamos abordar o t\'opico Unit Testing, utilizado para testar os m\'etodos criados com finalidade de encontrar erros de constru\c{c}\~ao;
 \item Tentar unir Unit Testing com JML (jml-junit) para testar asser\c{c}\~oes JML com Unit Testing.
\end{itemize}
Por fim ser\~ao descritas as dificuldades e conclus\~oes de desenvolvimento. 

\section{Do Alloy ao Java}

\subsection{Das Assinaturas \`as Classes}
As figuras seguintes representam respectivamente o metamodelo em Alloy e o diagrama de classes em Java.

\begin{center}
% use packages: array
\begin{tabular}{ll}
\includegraphics[scale=0.3]{meta-modelo.jpg} & \includegraphics[scale=0.3]{diagrama-classes.jpg}
\end{tabular}
\end{center}

Como se pode observar as figuras s\~ao bastante semelhantes. Com base no metamodelo foram criadas oito classes. As classes Seg, Semaphore, Track, State, Train, PointIn e PointOut equivalem \`a assinatura em Alloy com o mesmo nome. A classe abstracta Seg engloba todo o tipo de segmento existente. Um segmento pode ser uma agulha de sa\'ida (PointIn) , agulha de entrada (PointOut) e segmentos normais (Track). A classe abstracta Point representa as agulhas. Existem tamb\'em classes para representar os comboios (Train) e sem\'aforos (Semaphore). A classe State cont\'em os elementos necess\'arios para representar uma esta\c{c}\~ao seguindo o modelo anteriormente criado no Alloy. Todas as classes foram implementadas com uma vari\'avel \'unica chamada id para distinguir cada inst\^ancia da classe. Foram tamb\'em criadas excep\c{c}\~oes que s\~ao lan\c{c}adas quando ap\'os uma opera\c{c}\~ao, n\~ao existe mudan\c{c}a de estado.

\newpage

De seguida para cada rela\c{c}\~ao em Alloy apresenta-se a sua representa\c{c}\~ao em Java, tendo em conta que cada rela\c{c}\~ao em Alloy \'e uma vari\'avel de inst\^ancia em Java:
\begin{itemize}
 \item \begin{description}
        \item[Em Alloy] Cada segmento est\'a relacionado com o segmento seguinte e com um sem\'aforo (seta nexT e sema no metamodelo).
	\item[Em Java] A classe Seg tem uma vari\'avel de inst\^ancia do tipo Seg(next) e outra do tipo Semaphore(sema).
        \end{description}
	\begin{verbatim}
    public abstract class Seg {
    	static int[] nexts;
        static int n;
        static int num_inst;
        public int id;
        public Seg next;
        public Semaphore sema;

        public Seg();
        public Seg(Seg n_next, Semaphore n_sema);
        public Seg(Seg s);
        public Seg getNext();
        public void setNext(Seg next);
        public Semaphore getSema();
        public void setSema(Semaphore sema);
        public static int getNum_inst();
        public int getId();
    }
	\end{verbatim}
	As duas primeiras vari\'aveis de classe ser\~ao explicadas mais \`a frente. Em rela\c{c}\~ao aos m\'etodos, podemos ver get's e set's tr\^es construtores.
	
\item \begin{description}
        \item[Em Alloy] Cada segmento do tipo Track tem um conjunto de segmentos que lhe est\~ao sobrepostos (seta overlaps no metamodelo).
        \item[Em Java] A vari\'avel de inst\^ancia \'e do tipo ArrayList de Seg(overlaps).
        \end{description}
        \begin{verbatim}
    public class Track extends Seg {
        private ArrayList overlaps;

        public Track();
        public Track(Seg n_next, Semaphore n_sema, ArrayList n_overlaps);
        public Track(Track t);
        public ArrayList getOverlaps();
        public Object clona();
    }
    \end{verbatim}
    
    Al\'em da vari\'avel de inst\^ancia, existem tr\^es construtores, um get e o m\'etodo clona() que tem o mesmo comportamento que o m\'etodo clone() da classe Object.
    
\item \begin{description}
        \item[Em Alloy] Cada agulha de entrada est\'a relacionada com uma agulha de sa\'ida (seta prox no metamodelo).
        \item[Em Java] A classe PointIn tem uma vari\'avel de inst\^ancia do tipo PointOut(prox).
        \end{description}
    \begin{verbatim}
    public class PointIn extends Point  {
        public PointOut prox;

        PointIn(PointOut prox);
        PointIn(PointIn pi);
        public Object clona();
    }
    \end{verbatim}
   Al\'em da vari\'avel de inst\^ancia, existem dois construtores e o m\'etodo clona() explicado anterioremente.
\item \begin{description}
        \item[Em Alloy] Um estado tem a rela\c{c}\~ao tern\'aria entre estado , comboio e segmento; o conjunto de sem\'aforos a vermelho e o conjunto de agulhas com a sua posi\c{c}\~ao ON (seta  trains[Train] ; reds e ons respectivamente, no metamodelo).
        \item[Em ] A classe State tem 3 vari\'aveis de inst\^ancia, uma do tipo HashMap em que a chave \'e do tipo Train e o valor do tipo Seg(trains) ; uma do tipo ArrrayList de Semaphore (reds) e outra do tipo ArrayList de Point (ons).
        \end{description}
    \begin{verbatim}
    public class State {
        public HashMap trains;
        public ArrayList reds;
        public ArrayList ons;

        public State();
        public State( HashMap n_trains, ArrayList n_reds, ArrayList n_ons);
        private void moveTrain(Train t) throws CantMoveException;
        private void addTrain(Train t,Seg s)  throws CantAddTrainException;
        public HashMap getTrains();
        public void setTrains(HashMap n_trains);
        public ArrayList getReds();
        public void setReds(ArrayList n_reds);
        public ArrayList  getOns();
        private void setOns(ArrayList n_ons);
        private void setRed(Seg t);
        private void setGreen( Seg t) throws CantSetGreenException;
        public void toRed(Seg t) throws CantSetRedException;
        public void toGreen(Seg t) throws CantSetGreenException;
        public void move(Train t,Seg s)  throws CantMoveException;
        private boolean agulha_off(PointIn seg);
        public void toOff(PointIn pi, PointOut po) throws CantSetOffException;
        private void setOff(PointIn pi, PointOut po) throws CantSetOffException;
        public void toOn(PointIn pi, PointOut po) throws CantSetOnException;
        private void setOn(PointIn pi,PointOut po) throws CantSetOnException;
        public static void main(String args[]);
        public String toString();
    }

    \end{verbatim}
    
    \'E nesta classe que se encontram as opera\c{c}\~oes (move(), toRed(), toGreen(), toOn() e toOff()) juntamente com m\'etodos auxiliares (moveTrain(), addTrain() e agulha\_off()). Como nas outras classes existem os construtores, get's e set's.
    
\end{itemize}

O programa Java que desenvolvido foi implementado em Java 1.4 pois a ferramenta por n\'os utilizada (ESC/Java2) assim nos obriga.

\subsection{Das Regras da Esta\c{c}\~ao \`as especifica\c{c}\~oes em JML}

A maior parte das regras, definidas em Alloy, a que uma esta\c{c}\~ao deve obedecer transformam-se em invariantes em JML, com a particularidade de cada regra ser direcionada \`a inst\^ancia da classe em Java e n\~ao a todas as inst\^ancias geradas em Alloy. Outras regras por constru\c{c}\~ao da classe j\'a obedecem \`as regras em Alloy.

\begin{enumerate}
\item \begin{description}
        \item[Em Alloy] Cada segmento s\'o pode ter no m\'aximo um sem\'aforo.
            \begin{verbatim}
	sema in Track lone -> Semaphore
\end{verbatim}
        \item[Em Java] A vari\'avel de inst\^ancia da classe Seg obedece a essa regra.
\begin{verbatim}
	public Semaphore sema;
\end{verbatim}
       \end{description}


\item \begin{description}
       \item[Em Alloy] Devem existir sem\'aforos em todos os cruzamentos.
\begin{verbatim}
	all t : Seg | t in overlaps.Seg => one t.sema
\end{verbatim}
\item[Em Java] Foi adicionado o seguinte invariante na classe Track
\begin{verbatim}
	invariant (\forall int i; i >= 0 && i < overlaps.size(); 
                        ((Track) overlaps.get(i)).sema != null);
\end{verbatim}

       \end{description}


\item \begin{description}
       \item[Em Alloy] Cada segmento s\'o pode ser o seguinte de um segmento.
        \begin{verbatim}
	nexT & (Track -> Track) in Track lone-> Track
\end{verbatim}
\item[Em Java] Na classe Seg, criou-se uma vari\'avel de classe do tipo array de inteiros (nexts) de tamanho n que cont\'em os identificadores de todos os segementos que s\~ao os seguintes de algum segmento. Depois em todos os construtores, quando se especifica o segmento seguinte (n\_next) adiciona-se a pr\'e-condi\c{c}\~ao que indica que o n\_next nao pode j\'a ser seguinte de outro segmento.
        \begin{verbatim}
	//invariante da classe Seg
	invariant n == nexts.length && nexts != null;
	//pre condicao de todos os construtores da classe Seg
	requires (\forall int i; i >= 0 && i < nexts.length ; nexts[i] != n_next.id);
	requires n < nexts.length;
        \end{verbatim}
        
        \end{description}

\item\begin{description}
      \item[Em Alloy] Cada segmento n\~ao pode ser o seguinte de si pr\'oprio nem estar sobreposto a si mesmo.
        \begin{verbatim}
	all t:Seg | t not in t.nexT &&  t not in t.overlaps
        \end{verbatim}
        \item[Em Java] Na classe Seg e na classe Track respectivamente adicionaram-se os seguintes invariantes.
        \begin{verbatim}
	invariant this != this.next;
	invariant !overlaps.contains(this);
        \end{verbatim}
      \end{description}

\item \begin{description}
       \item[Em Alloy] Um segmento n\~ao pode ser seguinte e sobreposto de um outro segmento.
        \begin{verbatim}
	all t1,t2:Seg | t1->t2 in nexT => t1->t2 not in overlaps
        \end{verbatim}
        \item[Java] Na classe Track foi adicionado o seguinte invariante:
        \begin{verbatim}
	invariant this.next != null ==> !overlaps.contains(this.next);
        \end{verbatim}
        \end{description}

\newpage

\item \begin{description}
       \item[Em Alloy] Se o segmento A est\'a sobreposto ao segmento B, ent\~ao o segmento B est\'a sobreposto ao segmento A.
        \begin{verbatim}
            all t1,t2:Seg | t1->t2 in overlaps => t2->t1 in overlaps
        \end{verbatim}
        \item[Em Java] Na classe Track foi adicionado o seguinte invariante:
        \begin{verbatim}
	invariant (\forall int i; i>=0 && i < overlaps.size();
	               ((Track) overlaps.get(i)).overlaps.contains(this));
        \end{verbatim}
        \end{description}

\item \begin{description}
       \item[Em Alloy] Todas as agulhas de sa\'ida (PointOut) t\^em um sem\'aforo.
        \begin{verbatim}
            all p_out : PointOut | p_out in Seg => one p_out.sema
        \end{verbatim}
        \item[Em Java] Na classe PointOut colocou-se o seguinte invariante:
        \begin{verbatim}
            invariant this.sema != null;
        \end{verbatim}
        \end{description}

\end{enumerate}

\subsection{Dos Invariantes de segura\c{c}a \`as especifica\c{c}\~oes em JML}

Os invariantes em Alloy que indicam quando uma esta\c{c}\~o \'e segura est\a~o representados na classe State. Recordando a classe State, existe uma vari\'avel trains do tipo HashMap com chave do tipo Train e valor do tipo Seg.
\begin{itemize}
\item \begin{description}
        \item[Em Alloy] No mesmo segmento se encontra mais que um comboio.
        \begin{verbatim}
	pred one_train[s:State]{
	    all t:Track | lone t.~(s.trains)
	}
        \end{verbatim}
        \item[Em Java] Em vez de procurar em todos os segmentos se existe mais do que um comboio, basta dizer que nos valores do HashMap n\~ao existem repetidos, em Java um Set n\~ao tem elementos repetidos:
        \begin{verbatim}
	invariant trains.keySet().size() == trains.entrySet().size();
        \end{verbatim}

 \end{description}
\item \begin{description}
        \item[Em Alloy] Estando o comboio C no segmento S, n\~ao podem existir um comboios em segmentos sobrepostos a S.
        \begin{verbatim}
	pred train_overlap[s:State] {
	    all t1,t2 : Train | t1 + t2 in (s.trains).Track =>
	        t2.(s.trains) not in (t1.(s.trains)).overlaps
	}
        \end{verbatim}
        \item[Em Java] Traduz-se no seguinte invariante, tentando descrever: Para todos os segmentos sobrepostos a cada segmento em que se encontra um comboio, n\~ao podem estar nos valores do HashMap trains, pois se estiverem \'e sinal que existe um comboio nesse segmento, logo colis\~ao.
        \begin{verbatim}
	invariant (\forall int i;i>=0 && i< trains.size(); 
	  trains.values().toArray()[i] instanceof Track &&
	    (\forall int j;j>=0 && j < ((Track) trains.values().toArray()[i]).overlaps.size();
	      !trains.containsValue(((Track)trains.values().toArray()[i]).overlaps.get(j))));
        \end{verbatim}
\end{description}
\end{itemize}

\newpage

\subsection{Das Opera\c{c}\~oes aos M\'etodos}

Existem cinco opera\c{c}\~oes que alteram o estado de uma esta\c{c}\~ao. Em Java cri\'amos m\'etodos na classe State, um para cada opera\c{c}\~ao:

\subsubsection{Move}

Este m\'etodo inclui ainda moveTrain, addTrain, agulhas\_off como m\'etodos auxiliares;

\begin{description}
 \item[C\'odigo Alloy] \begin{verbatim}
 
pred move[s:State, s':State] {
        some t : Train {
            t not in ((s.trains).Seg)=>
                add_Train[s,s',t]
            else
            let track = t.(s.trains) {
                agulha_off[s,track] && (s.trains).(track.prox) = none=>
                    s'.trains = s.trains  - ( t -> track ) + (t -> track.prox) &&
                         s'.reds=s.reds && s'.ons = s.ons 
                else
                (    (  not (   one (track.nexT).sema && (track.nexT).sema in s.reds) ) && 
                    (s.trains).(track.nexT) = none ) =>
                            ( move_Train[s,s',t] )
                 else s'.trains = s.trains && s'.reds = s.reds && s'.ons = s.ons
            }
        }
}
\end{verbatim}
\item[C\'odigo Java] \begin{verbatim}

public void move(Train t,Seg s)  throws CantMoveException{
    try{
        if (this.trains != null && !this.trains.keySet().contains(t) && s!=null){
            this.addTrain(t,s);
        }else{
            if (this.trains != null && this.trains.keySet().contains(t)) {
                Object track = this.trains.get((Object)t);
                if ((track instanceof PointIn)) {
                    PointIn pi = (PointIn) track;
                    if (agulha_off(pi)) {
                        this.trains.remove(t);
                        this.trains.put(t, pi.prox);
                    } else throw new CantMoveException(new String("Agulha on!!!\n"));  
                } else {
                    if ((track instanceof Track)) {
                        Track trk = (Track) track;
                        if (!(trk.sema != null && this.reds != null && 
                              this.reds.contains(trk.sema)) && 
                              (!this.trains.containsValue(trk.next))){ 
                            this.moveTrain(t);
                        }else {throw new CantMoveException();}
                    }
                }
            }
        }
    }catch(Exception e){
            throw new CantMoveException("");
    }
}
\end{verbatim}
\end{description}

O c\'odigo Java do m\'etodo \'e baseado no c\'odigo Alloy. Vamos destacar as seguintes diferen\c{c}as entre o c\'odigo Alloy e Java:

\begin{itemize}
 \item Saber se um  comboio est\'a na/o esta\c{c}\~ao/estado, 
        \begin{description}
         \item[C\'odigo Alloy] train in (estado.trains).Seg
         \item[C\'odigo Java] trains.keySet().contains(train);
         \end{description}
 \item Accesso ao segmento em que se encontra o comboio.
\begin{description}
         \item[C\'odigo Alloy] let track = train.(estado.trains) \{...\}
         \item[C\'odigo Java] track = trains.get(train);
         \end{description}
 \item Filtrar os segmentos do tipo agulha de sa\'ida (PointIn)
\begin{description}
         \item[C\'odigo Alloy] interceptar o segmento com a rela\c{c}\~ao de todos os segmentos do tipo espec\'ifico (seg \& PointIn != null)
         \item[C\'odigo Java] express\~ao boleana que nos indica se o segmento \'e da inst\^ancia da classe PointIn (seg instanceof PointIn);
         \end{description}
 \item Remover/adicionar um elemento a um rela\c{c}\~ao tern\'aria (Estado,Comboio,Segmento)
\begin{description}
         \item[C\'odigo Alloy] s.trains -/+ (train $\rightarrow$ track)
         \item[C\'odigo Java] trains.remove(train) / trains.put(train,track).
         \end{description}
\end{itemize}

\subsubsection{ToRed, ToGreen}

Estes m\'etodos incluem respectivamente SetRed e SetGreen como m\'etodos auxiliares;

\begin{description}
 \item[C\'odigo Alloy] \begin{verbatim} 
 
 
 pred to_red[s:State, s':State] {
       	//pre   
    some sem : Semaphore {
        sem in Seg.sema
        sem not in s.reds
       		//pos
        s'.trains = s.trains
        s'.reds = s.reds + sem
        s'.ons = s.ons
    }
}

 
pred to_green[s:State, s':State] {
        some sem : Semaphore {
                sem in Seg.sema
                sem in s.reds
                let track = sema.sem {
                    (    track & Track != none && (track.overlaps).sema in s.reds && 
                    (track.overlaps &  Train.(s.trains)) = none    )   or
                    (track & PointOut != none &&  track in s.ons  )

                }
                s'.trains = s.trains
                s'.reds = s.reds - sem
                s'.ons = s.ons
        }
}



\end{verbatim}
\item[C\'odigo Java] \begin{verbatim}

public void toRed(Seg t) throws CantSetRedException{
	   if (this.reds!= null && t != null && !this.reds.contains(t.sema)) this.setRed(t); 
	   else throw new CantSetRedException();
	}
	
private void setRed(Seg t){
	  this.reds.add(t.sema);
	}

public void toGreen(Seg t) throws CantSetGreenException{
	  if (this.reds != null && t.sema != null && this.reds.contains(t.sema))
	     this.setGreen(t);
	} 
	

private void setGreen( Seg t) throws CantSetGreenException {
    if(t instanceof Track){
    Track tr = (Track) t;
    ArrayList over = tr.getOverlaps();
    if(over!=null){
        for(int i=0;i<over.size();i++){
            Track overlap = (Track) over.get(i);
            if(!this.reds.contains( overlap.sema )){
                throw new CantSetGreenException();
            }
            if(trains.containsValue(overlap)){
                //comboio nas overlaps
                throw new CantSetGreenException();
            }
        }
    }
    reds.remove(t.sema);
    }else if(t instanceof PointOut){
        if(!ons.contains(t)){
            //PointOut nao esta ON
            throw new CantSetGreenException();
        }
        reds.remove(t.sema);
    }
}

\end{verbatim}
\end{description}

Como podemos ver o c\'odigo Java \'e mais complexo pelo facto de se verificar a exist\^encia de vari\'aveis a null. Podemos destacar as seguintes diferen\c{c}as:

\newpage

\begin{itemize}
 \item Saber se um sem\'aforo est\'a a vermelho.
        \begin{description}
         \item[C\'odigo Alloy] sem in reds
         \item[C\'odigo Java] reds.contains(sem);
         \end{description}
 \item Remover/adicionar um elemento a um conjunto.
\begin{description}
         \item[C\'odigo Alloy] reds -/+ sem
         \item[C\'odigo Java] reds.add(sem) / reds.remove(sem);
         \end{description}
 \item Saber se os sem\'aforos dos segmentos sobrepostos ao segmento seg est\~ao a vermelho.
\begin{description}
         \item[C\'odigo Alloy] overlaps.Semahpore in reds
         \item[Em Java] Na classe State \'e necess\'ario percorrer todos os sem\'aforos dos segmentos que est\~ao sobrepostos, aos segmentos em que se encontram comboios (varia\'avel trains), na e verificar se est\~ao no conjunto reds.
         \end{description}
\end{itemize}

\subsubsection{ToOn, ToOff}

Os m\'etodos toOn() e toOff() incluem ainda setOn() e setOff() como m\'etodos auxiliares;

\begin{description}
 \item[C\'odigo Alloy] \begin{verbatim}

pred to_on[s,s' : State] {
	
 some p_out : PointOut  {
	 some p_in : PointIn {
	 p_in.prox = p_out
	 p_out + p_in not in s.ons
	 (s.trains).p_out = none
	 s.trains).p_in = none
	 s'.reds = s.reds
	 s'.trains = s.trains
	 s'.ons = s.ons + p_out + p_in
		}
	}
} 

pred to_off[s,s' : State] {

    some p_out : PointOut  {
        some p_in : PointIn {
            p_in.prox=p_out
            p_out + p_in in s.ons
            (s.trains).p_out = none
            (s.trains).p_in = none
            p_out.sema + p_in.sema in s.reds
            s'.reds = s.reds
            s'.trains = s.trains
            s'.ons = s.ons - p_out - p_in
        }
    }
}
\end{verbatim}

\newpage

\item[C\'odigo Java] \begin{verbatim}

public void toOn(PointIn pi, PointOut po) throws CantSetOnException{
		 if(this.ons!=null && pi!=null && po!=null && !this.ons.contains(pi) && !this.ons.contains(po)) setOn(pi,po);
		  else throw new CantSetOnException();
	}
	
	
	private void setOn(PointIn pi,PointOut po) throws CantSetOnException{
		 if(!trains.containsValue(po) && !trains.containsValue(pi)) {
		 	  ons.add(pi);
			  ons.add(po);
		 }else{
			  throw new CantSetOnException();
		}
	}


public void toOff(PointIn pi, PointOut po) throws CantSetOffException{
    if(this.ons!=null && pi!=null && po!=null && 
            this.ons.contains(pi) && this.ons.contains(po)){
        setOff(pi,po);
    }else { throw new CantSetOffException(); }

private void setOff(PointIn pi, PointOut po) throws CantSetOffException{
    //Se nao ha comboios nas agulhas e se o semaforo do POut esta a vermelho
    if(!trains.containsValue(po) && !trains.containsValue(pi) && 
            this.reds.contains(po.sema)){
        //Se o PI tiver semaforo tambem esta a vermelho
        if(pi.sema==null || this.reds.contains(pi.sema)){
           ons.remove(pi);
           ons.remove(po);
        }else{
           throw new CantSetOffException();
        }
    }else{
        throw new CantSetOffException();
    }
}


}
\end{verbatim}
\end{description}

Podemos destacar as seguintes diferen\c{c}as:

\begin{itemize}
 \item Saber se uma agulha est\'a na posi\c{c}\~ao ON
        \begin{description}
         \item[C\'odigo Alloy] point in ons
         \item[C\'odigo Java] ons.contains(point);
         \end{description}
 \item Alterar posi\c{c}\~ao da agulha
\begin{description}
         \item[C\'odigo Alloy] ons -/+ point
         \item[C\'odigo Java] ons.add(point) / ons.remove(point);
         \end{description}

\end{itemize}

\newpage

\section{Testing}

Numa fase final foram efectuados testes para verificar os resultados dos m\'etodos por n\'os criados.

\subsection{JUnit}

Numa primeira fase utilizamos JUnit, uma framework de Unit Testing para Java. No decorrer dos testes foram encontrados v\'arios erros de constru\c{c}\~ao de de acesso a objectos a null.


A classe de teste, onde ficam todos os m\'etodos utilizados para correr os testes est\'a definida como:

\begin{verbatim}
public class CasoDeTeste extends junit.framework.TestCase {
    
    private State estado;
    private Track t1,t2,t3,t4;
    private Train tr1;
    private PointIn p1;
    private PointOut p2;
    private Semaphore sema1;
    private Semaphore sema2;
    private Semaphore sema3;

    protected void setUp(){
        estado = new State();
        ArrayList over = new ArrayList();
        over.add((Seg) t4);
        t1 = new Track();
        t2 = new Track();
        t3 = new Track();
        t4 = new Track();
        tr1 = new Train();
        sema1 = new Semaphore();
        sema2 = new Semaphore();
        sema3 = new Semaphore();
        p2 = new PointOut(sema2);
        p1 = new PointIn(p2);
    }

    public static Test suite(){
        TestSuite suite= new TestSuite(State.class);
        return suite;
    }
}
\end{verbatim}


Exemplos de um m\'etodos de teste, para a seguinte topologia:

\begin{tabular}{lll}
\xymatrix{
                     & &                                  &                                  &\\
\ar@{|=}[rrr]^(.1)A  & & \ar@{|=>}[rr]^(.1)B_(.05)\rotimes &  &\\
                    & \ar@{|=>}[uu]^(.1)C_(.05)\rotimes &                                  & 					 &\\
                    & &                                  &                                  &\\
}
\end{tabular}

\begin{verbatim}
public void testComplex1(){

    t2.setNext((Seg) t1);
    t3.setNext((Seg) t2);
    ArrayList over = new ArrayList();
    over.add((Seg) t4);
    t3.overlaps = over;
    t4.sema = sema1;
    t3.sema = sema2;
    estado.reds.add(sema2);
    try {
        estado.move(tr1, (Seg) t4);
    } catch (CantMoveException e) {
        System.out.println("Cant Move");
    }
    assertEquals(1, estado.reds.size());
    assertEquals(1, estado.trains.size());
}
\end{verbatim}

No m\'etodo testComplex1(), depois de definir a topologia e estado da esta\c{c}\~ao, usamos a opera\c{c}\~ao move(). Por fim verificamos se o estado final \'e o esperado, atrav\'es de asser\c{c}\~oes (m\'etodo assertEquals()).


\subsection{JML-JUnit}

Numa segunda fase compilamos o c\'odigo com JMLC e JUnit para podermos assim testar asser\c{c}\~oes e verificar em runtime que os invariantes por n\'os impostos n\~ao eram violados. Infelizmente, mesmo correndo os testes com jmljunit, n\~ao nos foi poss\'ivel verificar nada em concreto.

\newpage

\section{Conclus\~oes/Dificuldades}

Este foi um projecto com um n\'ivel de complexidade bastante elevado. As ferramentas para JML n\~ao est\~ao desenvolvidas o suficiente, logo existem erros que demoravam tempo a resolver mas que no fim n\~ao eram erros de c\'odigo mas falhas nas ferramentas que ainda est\~ao pouca ``maduras''.

A ferramenta ESC/Java2 tipicamente indica se o m\'etodo:
\begin{itemize}
 \item viola um certo invariante;
 \item pode aceder a um objecto (que pode n\~ao estar referenciado);
 \item pode aceder a uma posi\c{c}\~ao de um array (que pode n\~ao estar nos limites do array);
 \item cont\'em um ciclo infinito ou um ciclo nunca utilizado.
\end{itemize}

Em contra-partida:
\begin{itemize}
 \item \'e limitada ao Java 1.4, a fraca tipagem desta vers\~ao obriga a castings e a mais especifica\c{c}\~oes em JML. Para definir o tipo de um ArrayList ARRAY \'e necess\'ario esta instru\c{c}\~ao em JML: ``//@ set ARRAY.elementType == $\setminus$ type(TIPO)'', no caso de um HashMap a tipagem n\~ao foi poss\'ivel;
 \item a heran\c{c}a de m\'etodos, por exemplo: o m\'etodo clone(), torna-se dif\'icil com a quantidade de especifica\c{c}\~oes JML que o m\'etodo tem na classe Object. No nosso caso n\~ao foi poss\'ivel fazer essa heran\c{c}a, tivemos de criar um m\'etodo com o mesmo comportamento mas n\~ao com a mesma assinatura.
 \item pode dar erros imposs\'iveis, com invariantes mais complexos;
 \item pode n\~ao encontrar erros presentes.
\end{itemize}

Em suma, a utilidade desta ferramenta \'e bastante discut\'ivel. Para a complexidade deste projecto esta ferramenta talvez n\~ao seja a mais aconselhada.

A biblioteca JUnit revelou-se bastante \'util para a gera\c{c}\~ao de testes, que por sua vez permite a descoberta de erros de constru\c{c}\~ao. J\'a a liga\c{c}\~ao entre JML e JUnit n\~ao teve o mesmo proveito, gra\c{c}as \`a complexidade das especific\c{c}\~oes JML.

Em rela\c{c}\~ao ao projecto em geral, foi poss\'ivel transformar o modelo em Alloy num programa em Java, com especifica\c{c}\~oes em JML, e posteriormente a realiza\c{c}\~ao de testes.

\newpage

\begin{thebibliography}{10}

\bibitem{DJACK}
Software Abstractions Logic Language And Analysis
\author = Daniel Jackson

\bibitem{Hansen98}
Formalising Railway Interlocking Systems

\end{thebibliography}

\end{document}